COMMENT ⊗   VALID 00013 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.Sec(Introduction)
C00011 00003	
C00025 00004	.SEC(Propositional logic)
C00039 00005	.BEGIN NOFILL
C00041 00006	.SS(Truth,,P9:)
C00048 00007	A statement form ↓wff← which is always true, no matter what the
C00050 00008	.SS(Computation)
C00063 00009	.SS(Completeness results)
C00067 00010	.GROUP
C00070 00011	%7LEMMA 10%1
C00074 00012	.turn on "#"
C00076 00013	.BEGIN NOFILL
C00081 ENDMK
C⊗;
.Sec(Introduction)
.begin "locat"
.at "$D"⊂"%dD%4∞%1"⊃
.at "?λ"⊂"%dλ%1"⊃
The purpose of this project is to study the concepts of deduction,
truth and computation as they apply to several mathematical and 
computer science formalisms, and to observe how the relationships
between these ideas change from one formalism to another.  Traditional studies of formal systems
in mathematical logic emphasize the deductive and truth aspects.  This
involves a discussion of proof theory and model theory.  Until recently,
the emphasis in computer science has been the study of computational
devices to explicate programming languages.  In the past seven years
serious investigations into the mathematical nature of languages
have begun.  This has involved the discovery of mathematical models for
programming languages.  For example, the fixed point semantics introduced by 
D. Scott calls upon lattice theory to exhibit a model of type-free
λ-calculus.

Previous research papers have tended to investigate only one or two of the 
deduction-truth-computation trio.  However, an unpublished paper by 
C. Wadsworth initiates the study of relationships among all three.  None
of the results in this project are original, the novelty of this paper
is in bringing these results together.  

We can define here some concepts which apply to all sections of this 
project.

A study of deduction requires some proof theory.  In particular, we need
to describe what a "deductive system" or "formal theory" is.
A formal theory %6T%* is defined when the following conditions are
satisfied:

.BEGIN INDENT 5,5,5;

%21.%*  A countable set of symbols is  given as the symbols of %6T%*.
A finite sequence of symbols of %6T%* is called an %3expression%* of %6T%*.

%22.%* There is a subset of the expressions of %6T%* called the %3well-formed
formulas%* (abbreviated %3wffs%*) of %6T%*⊗↓There is usually
an effective procedure to determine whether a given expression is a  wff.←.

%23.%* A set of wffs is set aside and called the set of %3axioms%*
of %6T%*.## %6T%* is an %3axiomatic theory%* if there exists an effective
procedure for deciding whether a given wff is an axiom.

%24.%* There is a finite set of relations %6R%41%1,#...#,%6R%4n%1 on
wffs, called %3rules of inference%*. For each %6R%4i%1 there is a unique
positive integer %6j%* such that for every set of %6j%* wffs and each wff
%dA%* one can effectively decide whether the  given %6j%* wffs are in the
relation %6R%4i%1 to %dA%*, and if so, %dA%* is called a %3direct consequence%*
of the given wffs by virtue of %6R%4i%1.
.END

Let %gG%* be a set of wffs, and let %eP%* be a wff in the formal theory %6T%*.
We say %eP%3 is deducible from %gG%1 in %6T%1 (denoted %gG%5ε%4T%dP%1) 
if there exists a finite sequence of wffs
%eP%41%1,#...,#%eP%4n%1 such that %eP%4n%1#=#%eP%1 and for 1≤i≤n, %eP%4i%1
is either an axiom, a formula in %gG%* or is a direct
consequence of previous %dP%4i%1's by virtue of one of the rules
of inference.
The sequence of %eP%4i%1's is called a %3derivation of %eP%3 from %gG%1,
or a %3proof of %eP%3 from %gG%1.  
If %eP%1 is deducible from the empty set (actually, from the axioms of the 
theory), we write %5ε%4T%eP%1⊗↓Generally, we will
not use the subscript "T" on the symbol "%5ε%1"; the
theory we mean should be clear from context.←, and say %eP%1 is a %3theorem%1 or 
%eP%1 is %3provable in %6T%1.

.P3:
.P2:
.BEGIN INDENT 0,5; GROUP;
The following properties are results of the definition of consequence:

         1) If %gG%1⊂%gD%1, and %gG%5ε%eA%1, then %gD%5ε%eA%1.

          2) %gG%5ε%eA%1 if and only if there is a finite subset %gD%1
of %gG%1 such that %gD%5ε%eA%1.

          3) If %gD%5ε%eA%1, and, for
each %eB%1 in %gD%1,## %gG%5ε%eB%1 then %gG%5ε%eA%1.
.END

Note that a "proof" is a sequence of wffs with certain restrictions and also that it
is a proof "of" the last statement in the sequence.  Therefore, if you 
consider only the first n elements of the sequence you have a proof of
the n%8th%1 statement.  A given sequence of wffs can usually be checked against
the definition to determine whether the sequence is a proof or not.

A property is said to be %3decidable%1 if there exists an effective
procedure (algorithm) which can tell us whether or not the property holds.  This
is a purposefully vague definition as we can apply it to properties of
symbols ( is "x" a symbol of %6T%1?), strings of symbols (is "x" a wff?),
sets of wffs (is ?P deducible from set "x"?), sequences of wffs (is "x" a
proof?), etc.  In particular, a formal theory %6T%1 is called decidable if
for any wff ?P of %6T%1 there exists an effective procedure for deciding
whether or not ?P is provable in %6T%1.

Another property of formal theories which is of interest is whether or not
they are consistent.  A theory is %3consistent%1 if it contains no wff
such that both it and its negation are provable.  An equivalent
definition is that there exists an unprovable statement.  An inconsistent
theory is not very interesting; all the theories we study are 
consistent.  If a theory has a model then it is consistent.



A  %3model%* for an axiomatic theory is a  system⊗↓A non-empty set of objects
among which are established certain relationships← of objects,
chosen from some other theory and satisfying the axioms. That is,
to each object or primitive notion of the axiomatic
theory an object or notion of the other theory is correlated in such a way that 
the axioms become (or correspond to) theorems of the other theory.
The meanings which are intended to be attached to the symbols, formulas, etc.
of a given formal system, in considering the system as a formalization of an 
informal theory, we call an %3interpretation%* of the system. 
That is, the interpetation of the symbols, formulas, etc. are the objects, 
propositions, etc. of the informal theory which are correlated under the
method by which the system constitutes  a model for the informal theory.
Well-formed formulas have meaning only when an interpretation is given
for the symbols. An %3interpretation%* consists of a non-empty set %9D%*,
called the domain of the interpretation, and an assignment to each predicate
letter %dA%4j%1 of an n-place relation in %9D%*, to each function letter
%df%4j%1 of an n-place operation in %9D%*, and to each individual 
constant %da%4i%1 of some fixed element of %9D%*. Variables are thought of as
ranging over %9D%*.

For a given interpretation, a wff without free variables represents a statement
which is true or false.  A wff with free variables represents a relation
on the domain of the interpretation which may be true for some values of 
the free variables and false for others.  An interpretation is said to be
a %3model%1 for a theory, %6T%1, iff every theorem of %6T%1 is true for the
interpretation.  These ideas are made precise in section 3.2.

Computation suggests an algorithm, or, effective procedure.  We want to know how
we can mechanize the process of determining the provability and/or
truth of a wff in a theory %6T%1.  At first glance, one might want to say
that deducibility and computability are equivalent or at least more closely related 
than computability and truth.  However there are subtle differences, which
depend very much on the formalism being investigated.  

%3Completeness%1 is generally considered to be equivalence of truth and 
deducibility in a theory.  We refer to completeness among deducibility,
truth, and computability by the obvious extension of the notion.  Besides
general completeness, we can speak of completeness with respect to a 
particular interpretation or class of interpretations.  This distinction
narrows our discussion of truth in all models to truth in the chosen models.  This
idea surfaces in Elementary Number Theory where we show that it is incomplete
with respect to the standard interpretation (Intuitive Number Theory).

Each section of this project has roughly the same format.  We look at deduction,
truth, and computation separately, and then see how they relate to each other.

In Propositional Logic we find that the three ideas are equivalent.  The
deductive power and the model theory of Propositional Logic are well 
established.  For computation we describe the process of complementary
literal elimination (%7CLE%1), or ground resolution.

For predicate calculus we expand our computation scheme to general 
resolution.  Again we have completeness, that is, we can show we have
computation <=> deduction <=> truth.  However, we have a probem "deciding"
whether or not our computation will yield any results.  If a wff %7is%1
provable then computation will terminate successfully; and %7if%1
computation terminates we have an effective procedure for deciding
provability.  However we cannot put any bound on our computation.  We
have no way of knowing whether the program will terminate or not.  Thus
we have only a "partial" decision procedure, in that it only works for
wffs which are valid, or, equivalently (in this case), provable.

In Elementary Number Theory we look at what we mean by an algorithm (effectively
computable function) more closely, and prove that the formal system
is undecidable.  This also establishes the undecidability of Predicate
Calculus (which we had left hanging after showing the procedure we had
described did not provide a decision procedure).  We sketch G⊗odel's
incompleteness results (using the numbering scheme we so cleverly avoided
in proving completeness for Predicate Calculus), exhibiting a wff which
is true under the standard interpetation but not provable.

Thus in moving from Propositional Logic, through Predicate Calculus, to 
Elementary Number Theory, we begin with decidability and completeness,
we first lose decidability, and finally also completeness.


A generalized theorem about undecidability in section 4.4 tells us that every 
formalism in which we can express all recursive functions must be undecidable.  Thus
the only decidable theory in this project is Propositional Logic.

When studying the ?λ-calculus we run into a few surprises.  Intuitively we
expect to be able to equate termination of computation with the idea of
finding a "normal form".  This idea of computation takes the reduction rules
(inference rules) of the formal system and considers them as computational
rules.  A "normal form" is reached when no more reductions are possible.  This
would lead us to believe that terms without normal forms should be "different"
(distinguishable semantically) from those with normal forms.  However, this turns
out not to be the case. 

This unexpected fact initially caused C. Wadsworth to reject D. Scott's $D as
an adequate model for the ?λ-calculus.  Instead, Wadsworth described what he
called "normal models".  However, rather than look elsewhere for a model, he
later realized it would be better to look more closely at the idea of
computation.  A more adequate analysis of computation involves the concept
of a generalized normal form (head normal form) which gives much more satisfying
results with respect to the models.

We exhibit several examples of terms which are equal in the models but cannot
be proved so in the formalism.  This is not surprising since equations between
terms in the ?λ-calculus are functional equations, which yield an infinite
number of facts, and, in general, it is impossible to effectively axiomatize
all true equations of such a functional kind, due to G⊗odel's incompleteness
results.

If we restrict our attention to terms with normal forms, it is easily established
that we have deduction <=> truth <=> computation.  We also show that if we
allow "approximate normal forms" we get completeness in the limit, that is,
every term is the limit of its approximate normal forms.  Thus we can compute
the approximate normal forms of a term to get a closer and closer approximation
of the term itself.

We use the equivalent concepts of head normal form and solvability to show
that two terms are equal in the models iff they are head normal form equivalent
iff they are solvably equivalent.

Lastly, we look at LCF (Logic for Computable Functions).  This system was
developed by D. Scott just before he discovered the models of the ?λ-calculus.  It
is a form of typed ?λ-calculus which he developed as an alternative to the type-free
?λ-calculus since the typed models were easily established.  Scott felt that "formalism
without eventual interpretation is in the end useless".

LCF is a language for discussing properties of programs.  R. Milner
has implemented an interactive proof checker using LCF, see Milner [9].  In
this section we consider only "realistic" completeness.  We do not attempt to
provide an algorithm for establishing the provability of an arbitrary wff as we
already know this is impossible.  We are interested only in the closed terms of
ground type, called "programs".  We show that for this subset of LCF we have
deduction <=> truth <=> computation.

The formalisms discussed in this project are arranged in the order of their expressive
power (with the exception of
LCF and ?λ-calculus, which should be reversed).  Anything
which can be expressed in one formalism can be expressed in the
one following it.  This is one of the reasons why once we lost decidability and completeness
due to statements formalizable within the system they were gone forever.

I had originally intended to conclude this project with a section on LISP.  However,
at that time I did not know what a mammoth job I had undertaken.  For the interested
reader, everything I could have said and more can be found in J. Allen's 
%2ANATOMY OF LISP%1, soon to be published by McGraw-Hill, and
M.J.C. Gordon's
Ph.D. thesis "Models of Pure LISP", which can be obtained by writing to Mrs.
Margaret-Pithie, School of Artificial Intelligence, Forrest Hill, Edinburgh EH1 2QL.
.end "locat"
.SEC(Propositional logic)
.SS(The deductive sytem,,p10:)
Following the definition of formal theory given in the introduction
 we describe the formal theory of propositional logic.

.BEGIN GROUP;
1. Countable set of symbols:
.indent 5,5;
Propositional (or predicate) letters: %dA%1, %dB%1, %dC%1, ...,  %dZ%1,
and the same subscripted by natural numbers.

Propositional connectives: %5⊃%1, and %5~%1.

Three auxiliary symbols: (,#),#,.

We will use the symbols %eA%1, %eB%1, %eC%1, ...,%eZ%1, subscripted as
needed, for metavariables.
.END
.BEGIN GROUP;
2. Specific wffs of propositional logic are denoted by %dP%*, %dQ%*,....
The class of formulas consists of:
.indent 5,5;

a) Atomic formulas; i.e. the proposition letters %dA%*, %dB%*, ...

b) If ?P and ?Q are wffs then  ~?P and ?P⊃?Q are wffs.⊗↓For ease in reading, we can
anticipate the interpretation of "##" as an implication, thus "%eP###Q%1 may be
read "if %eP%1 then %eQ%1", or "%eP%1 implies %eQ%1".←

.begin turn off "{","}";
If %eP%* is a wff in which no proposition letters other than those in the
set 
{ %dA%41%1, ...%dA%4n%1} occur, then %eP%1 is said to be a formula in
the proposition letters  %dA%41%1, ...%dA%4n%1.
.end
.end

.BEGIN GROUP;
3. There are many ways of axiomatizing propositional logic. The following
set of axioms is due to Mendelson[8]:

If %eA%*, %eB%*, and %eC%* are any wffs of %6T%* then the following are axioms of
%6T%*:

.BEGIN INDENT 10,10;
%2A1%* ##(%eA%5⊃%1(%EB%5⊃%eA%1))

%2A2%1 ##((%eA%5⊃%1(%eB%5⊃%eC%1))%5⊃%1((%eA%5⊃%eB%1)%5⊃%1(%eA%5⊃%eC%1)))

%2A3%1 ##(((%5~%eB%1)%5⊃%1(%5~%eA%1))%5⊃%1(((%5~%eB%1)%5⊃%eA%1)%5⊃%eB%1))
.END

These are axiom schemas expressed in meta-variables over %6T%*; they
actually give us an infinite number of axioms. 
Any instance of one of these statement forms is an axiom.

One can check a given wff
to see if it is an axiom. Therefore Propositional logic is an example
of an axiomatic theory.
.END

.BEGIN GROUP;
4. The only rule of inference is %3modus ponens%*: %eB%* is a direct consequence
of %eA%* and %eA%5⊃%eB%1 by modus ponens; written
.BEGIN NOFILL;
		%eA%*,  %eA%5⊃%eB%1 
		__________
		    %eB%*
.END
We shall abbreviate "modus ponens" as %7MP%1.
.END

We introduce  more propositional connectives as abbreviations:

.BEGIN NOFILL;
		(%eA%5∧%eB%1) for (%5~%1(%eA%5⊃%1(%5~%eB%1))
		(%eA%5∨%eB%1) for ((%5~%eB%1)%5⊃%1%eA%1)
		(%eA%1≡%eB%1) for ((%eA%1%5⊃%eB%1)∧(%eB%1⊃%EA%1))
.END

We shall now adopt some conventions for elimination of parentheses, hopefully
making complicated expressions easier to read. First we will omit the outer
pair of parentheses, thus (%eA%5⊃%eB%1) may be written %eA%5⊃%eB%1, 
(%5~%eA%1) as %5~%eA%1. Secondly, when a form contains only one
binary connective, parentheses are omitted by association to
the left. Thus 
%eA%5⊃%eB%5⊃%eA%5⊃%eC%1 stands for ((%eA%5⊃%eB%1)%5⊃%eA%1)%5⊃%eC%1.

Thirdly, the connectives are ordered as follows: ≡, ⊃, ∨, ∧, ~ and the parentheses
are eliminated according to the rule that ≡ has greatest scope and ~ has 
the least.  That is, ~ applies to the smallest statement form following
it, then ∧ connects the smallest statement forms surrounding it, then
∨, ⊃ and finally ≡.

For example, ~?A∨?B ≡ ?A⊃?B∨~?C∧?A stands for ((~?A)∨?B)≡(?A⊃(?B∨((~?C)∧?A))).


Clearly, from the definition of proof we have:

%7LEMMA 1	%5ε%eA%1, for %eA%1 an axiom.

"Proof" is used in two senses.  A proof in the theory, as defined previously,
is a sequence of wffs of the theory such that the last is the statement
we wish to prove and each other wff in the sequence is an axiom or
follows by a rule of inference from two previous members of the sequence.
As is the case with the axioms, we represent an infinite number of
actual theorems and proofs by using metavariables to establish a
proof schema.  Then any instance of a "theorem schema" is a theorem
of the theory, just as any instance of an "axiom schema" is an axiom.

We also give proofs of statements %2about%* the theory, such as the 
deduction theorem and completeness theorems.  These proofs are
constructed by the "usual" mathematical methods and written in
English supplemented by mathematical symbols and symbols from the
theory we are discussing.  These are actually meta-theorems, since
they are theorems about the theory rather than of the theory.
However, throughout this paper we will refer only to theorems,
lemmas, etc., without continuing the distinction by using the terms
meta-theorems, meta-lemmas, meta-etc.

We shall prove the following lemma in the theory of Propositional Logic,
i.e., we construct a sequence of wffs in L⊗↓Throughout this paper we shall
refer to the formal theory of Propositional Logic as L.← such that the
last element of the sequence is the statement we wish to prove, 
and each other wff in the sequence 
is an axiom or follows from previous members of the sequence by %7MP%1.


.BEGIN NOFILL;GROUP;
.P11:
%7LEMMA 2%1       For any wff %eA,  %5ε%eA⊃A%1.

Proof: 
.BEGIN indent 10,10;FILL;
1) %e(A⊃((A⊃A)⊃A))⊃((A⊃(A⊃A))⊃(A⊃A))%1     is an instance of axiom
schema %7A2%1 with %eA%1 for %eA, (A⊃A)%1 for %eB%1, and %eA%1 for
%eC%1.

2)  %eA⊃((A⊃A)⊃A)%1      axiom schema %7A1%1 with %eA%1 for %eA, 
                                               (A⊃A) %1for %eB%1.

3)  %e(A⊃(A⊃A))⊃(A⊃A)    %1from 1) and 2) by %7MP%1.

4)  %eA⊃(A⊃A)%1          axiom schema %7A1%e, A%1 for %eA, A%1 for %eB%1.

5)  %eA⊃A%1              from 3) and 4) by %7MP%1.
.END
.END

We can extend our idea of proof by allowing "abbreviations" of proofs
in that we can use any previously proved theorem in our sequence
of statements as an abbreviation for its own proof.  One most helpful
such theorem is the deduction theorem.  It is common mathematical practice
to prove a statement %eB%1 on the assumption of some other statement
%eA%1, and then conclude that we have "%eA%1 implies %eB%1."  In
Propositional Logic this procedure is justified by the Deduction
Theorem.

.BEGIN NOFILL;turn off "{","}";GROUP;

%7THEOREM 3%1  (Deduction Theorem)
.BEGIN FILL;
      If %gG%1 is a set of wffs, and %eA%1 and %eB%1 are wffs, 
and %gG%e,AεB%1, then %gG%eεA⊃B%1.
      In particular, if %eA ε B%1, then %eε A⊃B%1.
.END

Proof:
.BEGIN FILL;
    Let %eB%41%e,...,B%4n%1 be a derivation of %eB%1 from %gG%e,A%1
(we write %gG%e,A ε B%1 for %gG%1 ∪ {%eA%1} %eε B%1, and in general,
%gG%e,A%41%e,...,A%4n%e ε B%1 for %gG%1 ∪ {%eA%41%e,...,A%4n%1} %eε B)%1
then %eB%4n%1=%eB%1, we shall use induction on i, 1≤i≤n, to show 
that if %gG%e,A ε B%4i%1 then %gG%e ε A⊃B%4i%1 for every i.
.END
.APART;
.GROUP;

If i=1, then
        1) %eB%4i%1 is an axiom:
	   %eε B%4i%1          by Lemma 1
	   %eε A⊃B%4i%1        by axiom schema %7A1%1 and %7MP%1
	   %gG%e ε A⊃B%4i%1    property 1) of consequence
.begin turn on "{","}";
					 (see {yon(P3)})
.end
	2) %eB%4i%1ε%gG%1
	   then %gG%eεB%4i%1 and %gG%eεA⊃B%4i%1## by %7A1%1 and %7MP%1
	
	3) %eB%4i%1=%eA%1
	   then by lemma 2  %eεA⊃B%4i%1 and %gG%eεA⊃B%4i%1  by property 1) of consequence
.APART;
.GROUP;

Suppose true for i<k≤n, then 
	1) %eB%4k%1 is an axiom
	2) %eB%4k%1ε%gG%1
	3) %eB%4k%1=%eA
   %1Each of these cases is treated exactly as above.
        4) %eB%4k%1 follows by %7MP%1 from %eB%4i%1 and %eB%4j%1, i,j<k, where %eB%4j%1 = %eB%4i%1⊃%eB%4k%1
	   %gG%e ε A⊃B%4j%1     by inductive hypothesis
	   %gG%e ε A⊃B%4i%1     by inductive hypothesis
	   %eε (A⊃(B%4i%e⊃B%4k%e))⊃((A⊃B%4i%e)⊃(A⊃B%4k%e))%1   %7A2%1
	   %gG%e ε A⊃B%4k%1     by %7MP%1 twice (noting that %eB%4j%1=%eB%4i%e⊃B%4k%1)
The theorem follows as the special case where i=n.
.END

Now that we have the deduction theorem the proof of Lemma 2 is simplified
to the point of being trivial.
.BEGIN NOFILL;

.group;
%7LEMMA 2%1   For any wff %eA, ε A⊃A%1.
Proof:
	Clearly, %eA ε A%1 by the definition of proof, therefore
	by the deduction theorem %eε A⊃A
     
.apart
.GROUP
%1The following lemma gives us a transitivity rule for implication.

%7LEMMA 4%e     A⊃B, B⊃C ε A⊃C
%1Proof:
	1) %eA⊃B%1        hypothesis
	2) %eB⊃C%1	  hypothesis
	3) %eA%1	    hyp.
	4) %eB%1	    1) and 3) %7MP%1
	5) %eC%1	    2) and 4) %7MP%1
Thus %eA⊃B, B⊃C, A ε C%1, so, by the deduction theorem %eA⊃B, B⊃C ε A⊃C%1.
.END
.BEGIN NOFILL;
.GROUP;

%7LEMMA 5%1   %e(~B⊃~A)⊃(A⊃B)
%1(Proof by contradiction is valid)
Proof:
.BEGIN TABIT3(6,10,40);
\1)\%e~B⊃~A%1\hyp
\2)\%eA%1\hyp
\3)\%e(~B⊃~A)⊃((~B⊃A)⊃B)\%7A3%1
\4)\%EA⊃(~B⊃A)\%7A1%1
\5)\%e(~B⊃A)⊃B\%7MP%1, 	1) and 3)
\6)\%eA⊃B%1\4), 5), lemma 4
\7)\%eB%1\%7MP%1, 2) and 6).
.END
.END
Thus %e~B⊃~A,#A %5ε%eB%1. Therefore by the deduction theorem:
%e~B⊃~A#%5ε%eA⊃B%1. Therefore by the deduction theorem:
%5ε%e(~B⊃~A)⊃(%eA⊃B)%1.

.SS(Truth,,P9:)
For propositional logic, an interpretation needs only the domain set %9D%*, and
an assignment of an element of %9D%* to each proposition letter. We have no
variables to worry about or relations or functions among or on the objects of 
%9D%*. "~" and "⊃" ⊗↓ and thus "∧", "≡", and "∨"← are given their usual  meaning⊗↓"~"
is negation, "##" is an implication, and thus "∧" is conjunction "and"),
 "∨" is disjunction ("or"), and "≡" is equivalence.←
In this way every proposition letter can be assigned a truth value, true or
false, according to the value of its assigned elements in %9D%*.

The truth value of a wff is determined by the truth values of the proposition
statements making up its component parts.
We give these rules in metavariables to emphasize that the definitions
extend to %2any%* combination of propositions.

.GROUP
~ is negation; ~%eA%* is %3true%* iff %eA%* is %3false%1. Thus the 
following truth table:

.BEGIN NOFILL;SELECT E;

		A   ~A
		_______
		t    f
.apart
.END
.group
⊃ is a conditional %eA⊃B%1; read "If %eA%1 then %eB%*". Its meaning
is given by the following:

.BEGIN NOFILL SELECT E;
		A  B   A⊃B
		__________
		t  t    t
		f  t    t
		t  f    f
		f  f    t
.END
.apart
We are used to "If %eA%1 then %eB%1" implying some sort of causal relationship
in usual usage, however the truth-table entries of lines 2 and 4 can be justified
by considering the following possible interpretations:

"If %3x%* is an even integer, then %3x%1 is divisible by %32%1". We certainly don't
want to consider cases where %3x%1 is odd as counterexamples to the general 
assertion. Also, we want the statement "If %eA%1 and %eB%1, then %eB%1" to be
true in all cases.

.BEGIN NOFILL SELECT E;GROUP;
%1The truth tables for the connectives ∧, ∨, and ≡ are:%e

A  B  A∨B      	A  B  A∧B  	A  B  A≡B
_________      __________      __________
t  t   t	t  t   t	t  t   t
t  f   t	t  f   f	t  f   f
f  t   t  	f  t   f	f  t   f
f  f   f	f  f   f	f  f   t
.END

Each row of a truth table corresponds to a possible interpretation %gf%*.
If a wff %eP%* is made up of proposition letters %dP%41%1, ..., %dP%4n%1
and propositonal connectives, there are 2%8n%1 possible interpretations
%gf%4i%1 assigning truth values to the proposition letters. 
.group
For example %eA∨~C ≡ B%1⊗↓which is equivalent to %e((A∨(~C))≡B)← has the
following truth table:

.BEGIN NOFILL;SELECT E;
A  B  C  ~C  A∨~C   A∨~C≡B
_________________________
t  t  t  f    t		t 
t  t  f  t    t         t
t  f  t  f    t		f
t  f  f  t    t		f
f  t  t  f    f		f
f  t  f  t    t		t
f  f  t  f    f		t
f  f  f  t    t		f
.END
.apart
Truth tables can be abbreviated by simply writing the wff once, and
writing the possible assignments of truth value under each proposition
letter and, step by step, the truth values of each  component sentence
under the principal connective⊗↓the one applied last in constructing
the component← of that component. 

.BEGIN NOFILL;SELECT E;GROUP;
%1Thus:%*
		A ∨ ~ C ≡ B
		___________
		t t f t t t
		t t t f t t
		t t f t f f
		t t t f f f
		f f f t f t
		f t t f t t
		f f f t t f
		f t t f f f
.SELECT 1;
		                    1##3###2####1##4###1 ⊗↓numbers indicate the order in which 
columns are filled in←
.END

A statement form ⊗↓wff← which is always true, no matter what the
truth values of its statement letters⊗↓proposition letters← may be, is
called a %3tautology%1. Such a statement %eP%* is said to be %3valid%* or %3true
in all models%*, and is denoted by %5|%eP%1. If %eP%* is true in all models 
then %e~P%1 is false in all models; that is, there does not exist a model for
%e~P%1. We express this by saying that %e~P%1 is %3unsatisfiable%1.

The validity of any statement %eP%1 is decidable. %5|%eP%1 iff the column
under %eP%1 in its truth table (or under its main connective in abbreviated
form) contains only %et%1's. I.e. %gf%e(P)%1=%et%1 for every possible 
interpretation %gf%*.

.BEGIN NOFILL;group;
.P8:
%7LEMMA 6%1  [(P∧(P⊃Q)]⊃Q%1 is a tautology.  Hence if %eP%* and %eP⊃Q%1 are tautologies then so is %eQ%*.

Proof:
.SELECT E;GROUP;
P  Q   P⊃Q   P∧(P⊃Q) [(P∧(P⊃Q)]⊃Q
_________________________________
t  t	t	t	t
t  f	f	f	t
f  t	t 	f	t
f  f	t	f	t
.END

.SS(Computation)
Now that we have developed the ideas of deducibility (provability) and 
truth, we want to know what computability can mean in propositional logic.
Then we can discuss the relationships between these ideas.

Computation for propositional logic will be based on the idea of 
%3complementary literal elimination%1⊗↓Hence forth 
called %7CLE%1.←, also called %3ground resolution%1.
In order to develop this idea we introduce %5t%* and %5b%*⊗↓"%5b%*" may be read
"box", or "the empty clause", which is its eventual interpretation.← as
abbreviations for %e~P∨P%1 and %e~P∧P%1, respectively.
We also assume that our wffs are expressed using only the connectives ∧, ∨, and ~.
Clearly this is possible since ?P⊃?Q is just ~?P∨?Q and ?P≡?Q can be written
(?P∧?Q)∨(~?P∧~?Q).

A wff %eP%* is in %3conjunctive normal form%1 if:

.BEGIN INDENT 5,5;
%21.%1 No subformula %eQ%* of %eP%* whose principal connective is ~ contains
another occurrence of ~, or an occurrence of ∧, ∨, %5t%*, or %5b%*.

%22.%1 No subformula of %eP%* whose principal connective is ∨ contains an occurrence
of ∧, %5t%* or %5b%*. That is, there does not exist an occurrence of %5t%*,
%5b%* or ∧, within the scope of any ∨.

%23.%1 There does not exist %5t%* or %5b%* within the scope of any ∧.
.END

%eP%* is in %3reduced conjunctive form%1 if:

.BEGIN INDENT 5,5;
%24.%1 No proposition letter appears more than once within the scope of any ∨.

.end
Every wff %eP%* can be reduced to an equivalent formula %eP%1' such that %eP%1' is in
reduced conjunctive form by the following:
.begin indent 5,5;

%2a.%1 By repeated application of the following reduction rules we get a formula 
satisfying %21.%1 above;

.BEGIN NO FILL;
	  i. %e~~Q → Q%1   where "→" is to be read "reduces to".
	 ii. %e~(Q%41%*∧Q%42%*) → ~Q%41%*∨~Q%42%1
	iii. %e~(Q%41%*∨Q%42%*) → ~Q%41%*∧~Q%42%1
	 iv. %e~%5t%* → %5b%1
	  v. %e~%5b%* → %5t%1
.END
%2b.%* the following rules eliminate occurrences of ∧, %5t%* or %5b%* within
the scope of any ∨.

.BEGIN NOFILL;
	  i. %eQ%41%*∨(Q%42%*∧Q%43%*) → (Q%41%*∨Q%42%*)∧(Q%41%*∨Q%43%*)%1
	 ii. ∨ and ∧ are commutative operations
	iii. %eQ∨%5t%* → %5t%1
	 iv. %eQ∨%5b%* → Q%1
.END

%2c.%* we insure no occurrences of %5t%* or %5b%* with the scope of any ∧ by:

.BEGIN NOFILL;
	  i. %eQ∧%5t%* → Q%1
	 ii. %eQ∧%5b%* → %5b%1

.END
%2d.%* To put our formula in %2reduced%* conjunctive form we eliminate repetitions
of the same proposition letter within the scope of any ∨ as follows:

.begin indent 7,7;
Assume %eP%* is in conjunctive form. Let %eQ%* be a subformula of %eP%*
of the form %eP%41%*∨%eP%42%1. By condition %22%* of conjunctive normal
form we know %eP%41%1 and %eP%42%1 are built up by ∨'s from 
%dP%4i%1's and ~%dP%4i%1's where each %dP%4i%1 is a proposition letter.
"∨" is both associative and commutative so we can rearrage the
%dP%4i%1's and ~%dP%4i%1's so that if %eQ%1 contains two occurrences of some 
%dP%4k%1 we can assume %eQ%* contains some subformula of the form:
.end
.NOFILL

	  i. %dP%4k%*∨P%4k%1 which reduces to: %dP%4k%1
	 ii. %1~%DP%4k%*∨P%4k%1 which reduces to: %5t%1
	iii. %1~%DP%4k%*∨%1~%DP%4k%1 which reduces to:~%dP%4k%1

.END
We shall now describe the process of %7CLE%1 on formulas in reduced
conjunctive form. First some definitions:⊗↓The following style of syntax specification,
called BNF (Backus-Naur Form) equations, has the same intent as that of inductive
definitions.  The symbol "::=" is to be read "is a"; the symbol "|" is to be read
"or"; and juxtaposition of x and y is to be read "x followed by y".←

.BEGIN NOFILL;
 	<+literal>::= <proposition letter>
	<-literal>::= %e~%1<proposition letter>
	<ground clause>::= %5b%1 | <%5+%1literal> | <%5+%1 literal> ∨ <ground clause>
	<ground sentence>::= <ground clause> | <ground clause> ∧ <ground sentence>
.END
.FILL
%5b%1 is the empty clause. A wff in reduced conjunctive form is a ground
sentence.  The adjective "ground" refers to the fact that the clause or
sentence it precedes contains no variables.  Since there are no such animals
in Propositional Logic, all clauses and sentences are ground.  The distinction
will become more important in the next chapter.  We will abbreviate "ground"
by "gr".

Sometimes it is convenient in the following to think of a gr sentence as a set of gr
clauses, and a gr clause as a set of literals.  This will cause no 
confusion as we know that a gr sentence is a conjunction of its elements
(gr clauses), and a gr clause is a disjunction of its elements 
(<%5+%1literal>s).  Thus the following definitions:

.BEGIN NOFILL;
.turnoff"{","}"
	<gr clause>::= %5b%1 | {<%5+%1literal>} | {<%5+%1literal>} ∪ <gr clause>
	<gr sentence>::= {<gr clause>} | {<gr clause>} ∪ <gr sentence>
.turnon "{","}"
.END

%dP%4k%1 and ~%dP%4k%1 (where %dP%4k%1 is a proposition letter) are
%3complementary literals%1.
If %eA%1 and %eB%1 are gr clauses and %dP%4k%1ε%eA%1 and ~%dP%4k%1ε%eB%1,
then the %3ground resolvent%1 of %eA%1 and %eB%1 with respect to %dP%4k%1
and ~%dP%4k%1 is
.BEGIN center;
.turnoff "{","}" 
	(%eA%1-{%dP%4k%1}) ∪ (%eB%1-{~%dP%4k%1})
.turnon "{","}"
.END
That is, the complementary literals are eliminated in the resolvent 
clause, all else remaining unchanged.
Gr resolution, or %7CLE%1, is a more general application of %7MP%1,
which states that from %eA%1 and %eA⊃B%1, we can deduce %eB%1.
This could also be written: from  %eA ∧ (~A∨B)%1 (which is in reduced
conjunctive form) we can deduce %eB%1.  %7CLE%1 on %eA%1 and ~%eA%1
results in the gr resolvent %eB%1.
.BEGIN NOFILL;
     Ex.  1) %d(P∨Q) ∧ (R∨%1~%*P)
	   

		   Q ∨ R


	%12) %d(%1~%*P∨Q∨%1~%*R) ∧ R ∧ %1~%*Q


  	           %1~%*P ∨ Q


			%1~%*P%1
.END

Note that in the second example, the same result could have been obtained
by first resolving the %dQ%1's and then the %dR%1's. 

A %3resolution deduction%1 of a clause %eA%1 from a set of clauses
%eS%1 is a finite sequence of clauses %eB%41%e,...,B%4n%1 such that
.BEGIN NOFILL;
	1) %eB%4n %1is %eA%1
	2) ∀i, 1≤i≤n, %eB%4i%1 is either
	   	a) an element of %eS%1, or
		b) a ground resolvent of %eB%4j%1 and %eB%4k%1 where j,k<i.
.END									
If %eC%* is a ground resolvent of %eA%* and %eB%* we sometimes write: "%eA%1∧%eB%1→%eC%1".


%eS%5*%eA%1 if there exists a resolution deduction of %eA%1 from %eS%1.
A resolution deduction of %5b%1 from  %eS%1 is called a %3resolution refutation of%1
or simply a %3refutation of %eS%1.
.BEGIN NOFILL;group

.turnoff "{","}"
     	Ex. %eS%1={%d(P%41%d∨P%42%d), (%1~%*P%42%d∨P%43%d), (%1~%*P%41%d∨P%43%d), %1~%*P%43%1}

     	    %eB%41%1: %dP%41%d∨P%42%e        B%42%1: ~%dP%42%d∨P%43%e
	

		B%43%1: %dP%41%d∨P%43%e          B%44%1: ~%dP%41%d∨P%43%e


			B%45%1: %dP%43                %eB%46%1: ~%dP%43%e


		            B%47%1: %5b%1
.turn on "{","}"
.END

.FILL
Clearly there are many possible paths that a resolution may take.  One way to
mechanize the process is to take %7all%1 possible paths.

.P100:
Given an initial set of clauses %eS%1, we define %6R%1(%eS%1) to be the union
of %eS%1 with the set of all possible ground resolvents of clauses in %eS%1,
and %6R%8n+1%e(S)%1=%6R%e(%6R%8n%e(S))%1.
.P12:
.P5:
By definition, %eS%1⊂%6R%e(S)%1⊂%6R%82%e(S)%1⊂... .  Also each %6R%8n%e(S)%1⊂%eS%8*
%1, the set of all possible clauses using literals contained in %eS%1,
since no new literals are generated by ground resolution.  %eS%8*%1 is finite,
therefore for some integer m, which depends on %eS%1, we have 
%6R%8m%e(S)%1=%6R%8k%e(S)%1 for all k≥m. Thus the operation of taking
resolvents "closes out" (we get no new resolvent clauses) after a finite number 
of steps.
If %5b%1ε%6R%8m%e(S)%1, then there exists a refutation of %eS%1.  If 
%5b%5N%6R%8m%e(S)%1, then there does not exist a refutation of %eS%1.
Thus, given any set of clauses, %eS%1, it is decidable whether or not
%eS%5*b%1.

Clearly, as soon as %5b%1 appears we need go no further with the computation.
To crank out all of %6R%8m%e(S)%1 for every set of clauses, %eS%1, would be 
horribly inefficient, however, we are not presently concerned with efficiency.
For refinements of resolution procedures see D. Loveland [5].



.SS(Completeness results)
Now we would like to investigate the relationships between a statement
being provable, being true, and its negation being refutable.
 
.BEGIN NOFILL;GROUP;
%7LEMMA 7%1   If %eP%1 is an axiom, then %eP%1 is a tautology.
Proof: of %7A1%1 and %7A3%1 (%7A2%1 is left to the reader.)
.select e;

	A	B	B⊃A	A⊃(B⊃A)
    ______________________________________
	t	t	 t	 t
	t	f	 t	 t	
	f	t	 f	 t
	f	f	 t	 t

.APART;
.GROUP;
										
A  B ~B  ~A  ~B⊃~A  ~B⊃A  (~B⊃A)⊃B   (~B⊃~A)⊃((~B⊃A)⊃B)
________________________________________________________
t  t  f   f    t      t	       t	   t
t  f  t   f    f      t	       f	   t
f  t  f   t    t      t	       t	   t
f  f  t   t    t      f        t      	   t

.End

%7THEOREM 8%1  If %eεP%1 then %5|%eP%1  (if %eP%1 is provable, then
%eP%1 is a tautology).
.BEGIN NOFILL;
Proof:
.BEGIN INDENT 8,13;fill
	%eεP%1 implies that there exists a derivation of %eP%1, say
	%eP%41%e,...,P%4n%1=%eP%1, such that for all i, 1≤i≤n,
	 %eP%4i%1 is an axiom or %eP%4i%1 follows by %7MP%1 from
	%eP%4j%1 and %eP%4k%1=%eP%4j%e⊃P%4i%1 where j,k<i.
.END
	  We shall prove that each %eP%4i%1, 1≤i≤n, is a tautology by induction on i.
	   1) i=1, then %eP%4i%1 is an axiom, and by lemma 7 it is a tautology.
	   2) assume true for i<k, then %eP%41%e,...,P%4k-1%1 are tautologies.
.BEGIN INDENT 14,13;
		a) %eP%4k%1 is an axiom.  Then by lemma 7 %eP%4k%1 is a tautology.

               	b) %eP%4k%1 follows by %7MP%1 from %eP%4i%1 and %eP%4j%1 where
	     i,j<k.  %eP%4i%1 and %eP%4j%1=%eP%4i%e⊃P%4k%1 are tautologies by
	     the inductive assumption, therefore %eP%4k%1 is a tautology by
	     Lemma 6.
.END
	Therefore, %eP%4n%1=%eP%1 is a tautology.
.END


Thus deducibility implies truth.  Now we look at truth and computation.

%7LEMMA 9%1  If %eS%1 is an unsatisfiable set of gr clauses with %eA%1ε%eS%1,
and %eB%1⊂%eA,%1 then %eS%1 with %eA%1 replaced by %eB%1 is an unsatisfiable
set.
.BEGIN NOFILL;
Proof:
.BEGIN FILL;INDENT 10,10;
	%eA%1 is a disjunction of literals, %eB%1⊂%eA%1.  If %eS%1 with %eA%1
	replaced by %eB%1 is satisfiable, then there exists an interpretation
	%gf%1 such that clause %eB%1 is true.  A disjunction is true if
	any part of it is true, thus the same interpretation renders %eA%1
	true and is a model for %eS%1, thus %eS%1 is satisfiable, which
	contradicts our initial assumption.
	  Therefore %eS%1 with %eA%1 replaced by %eB%1 is unsatisfiable.
.END
.END
.GROUP;
A set ?S of clauses is a %3minimal unsatisfiable%*
set if ?S is unsatisfiable but no proper subset of
?S is unsatisfiable⊗↓A minimal unsatisfiable set is finite by
the Compactness Theorem.←.
.APART

Every unsatisfiable set contains a minimal unsatisfiable  subset, but such a
subset is not necessarily unique. 
.BEGIN TURN OFF "{","}";CENTER;
.group
For example:
		{%DA, B, %1~%*A, %1~%*B%1} has two minimally unsatisfiable subsets.
.apart
.END
We know such a subset exists since the set of integers, %3n%*, for which there
is an unsatisfiable subset of %eS%* with %3n%* clauses must have
a least integer %3n%*, and an unsatisfiable subset with %3n%* clauses
must therefore  be minimal.

A clause which contains only one literal is a %3unit clause%*.
A %3multi-unit clause%* is a clause with two or more literals. A %3non-unit clause%1
is either  the empty clause or a multi-unit clause. 

If %eS%* is a set of clauses, the phrase "%eS%* with %dA%* replaced by %dB%*"
denotes the set:
.BEGIN TURN OFF "{","}";CENTER;

		(%eS%1-{%DA%*})∪{%DB%*}

.END

.TURN OFF "#";
Let #%eS%1 denote the number of clauses in the finite set %eS%*, and
##%eS%1 the number of literal occurrences in %eS%*. The number of %3excess
literals%* of %eS%* is ##%eS%*-#%eS%* which is non-negative if %5bN%eS%1.

%7LEMMA 10%1
If %eS%* is a minimal unsatisfiable set of ground clauses
then %eS%5*b%1.

%2proof%*: (by induction on the number of excess literals)

.begin turn off "{","}";
If %5b%1ε%eS%*, then %eS%1 = {%5b%1}, since %eS%* is minimal and {%5b%1} %5*b%1.

Now assume %5bN%eS%1, then ##%eS%1-#%eS%1 ≥0.

.begin indent 10,10;FILL;
%21.%* If the number of excess literals is 0, there are no non-unit clauses 
in ?S. Thus ?S is of the form {%dP, %1~%*P%*} for some literal %dP%*. Then ground
resolution yields %5b%*.

%22.%* Assume true for all k<n, n>0. Since n>0, there exists
a multi-unit clause %eA%* in ?S. Let %dP%1ε%eA%1 and let ?S%41%1 be ?S
with %eA%* replaced by %eA-%1{%dP%1}. By Lemma 9, ?S%41%1 is unsatisfiable.
Let ?S' be a minimal unsatisfiable subset of ?S%41%1. ?S%41%1, and
thus ?S' has less than n excess literals. Therefore  by  the induction
hypothesis  ?S'%5*b%1 by some resolution deduction
%eB%41%1,...%eB%4k-1%1,%eB%4k%1=%5b%1. 
.begin indent 12,12;
a)If no %eB%4i%1 1≤i≤k is %eA%1-{%dP%1} then
%eB%41%1,#...,#%eB%4k%1, is also a refutation of ?S; 

b) if some %eB%4i%1 %2is%*
%eA%1-{%dP%1} we make %eB%41%1,#...,#%eB%4k%1 into a deduction from ?S by replacing
%dP%* in  %eA%1-{%dP%1}, to yield %eA%*, and adjusting subsequent resolvents
to include %dP%1 if necessary. Let %eB%41%1',..., %eB%4k%1' denote the deduction
from ?S so obtained.
.NOFILL;
		i) if %eB%4k%1'=%5b%1 we are done; otherwise:
		ii) %eB%4k%1'={%dP%1} since we had to add in %dP%1 all the
		way through the deduction.
.END


.FILL;
Now we obtain a refutation of %eT%1∪{%dP%1} for some subset %eT%1 of ?S and append it to 
%eB%41%1',...,%eB%4k%1' to get a refutation of ?S.

Let ?S%42%1 be ?S with %eA%1 replaced by {%dP%1}.  ?S%42%1 is unsatisfiable,
again by Lemma 9.  Let ?S%8**%1 be a minimal unsatisfiable subset of ?S%42%1.
?S%8**%1 is %eT%1∪{%dP%1} for some %eT⊂%1?S as {%dP%1} must be in
?S%8**%1.  Otherwise ?S%8**%1 would be a proper subset of ?S, but ?S
was a %3minimal%1 unsatisfiable set by hypothesis.

%eT%1∪{%dP%1} has fewer than n excess literals, so by induction hypothesis
there exists a refutation %eC%41%e,...,C%4r%1 of %eT%1∪{%dP%1}.
Then %eB%41%1',..., %eB%4k%1',%eC%41%1,...,%eC%4r%1 is the desired refutation
of ?S.
.end
.END

.turn on "#";
.BEGIN NOFILL;group;

%7THEOREM 11%1      %5|%eP%1 implies ~%eP%5*b%1
	(If ?P is true in all models, then there exists a refutation of ~?P )
Proof:  %5|%EP%1 iff ~?P is unsatisfiable.
	~?P is unsatisfiable implies that there exists a minimal
	unsatisfiable subset ?S of ~?P.  By Lemma 10, ?S%5*b%1,
	thus by the same refutation ~?P%5*b%1.
.END

Thus if a wff ?P is valid, we can compute a refutation of ~?P. Now we compare
computation with deduction:

.BEGIN NOFILL;group;

%7LEMMA 12%1  If ?Q is a ground resolvent of clauses in ?P, then %5ε%eP⊃Q%1. (?P→?Q  =>  %5ε?P⊃?Q)
Proof:
	?P→?Q  =>  ?P is of the form (?R∨?P1) ∧ (~?R∨?P2) ∧ ?P3
		where ?R is a proposition letter, ?P1 and ?P2 are clauses,
		and ?P3 is a conjunction of clauses; and ?Q=(?P1∨?P2), then:
	[(?R∨?P1) ∧ (~?R∨?P2)∧?P3] %5ε ?Q, can also be written:
	~?P1⊃?R, ?R⊃?P2, ?P3 %5ε%e (~P%41%1⊃?P2)
	~?P1⊃?R, ?R⊃?P2 %5ε%1 ~?P1⊃?P2   by Lemma 3
	%5.%1 (~?P1⊃?R)∧(?R⊃?P2) %5ε%1 (~?P1⊃?P2) or, (?R∨?P1)∧(~?R∨?P2)∧?P3 %5ε%1 (?P1∨?P2)
	that is, ?P %5ε%1 ?Q  and by the Deduction theorem we have, %5ε ?P⊃?Q
.END


.BEGIN NOFILL;
.group;
%7LEMMA 13%1    ~?P%5*?Q => %5ε~?P⊃?Q 
Proof:
	~?P%5*?Q => there exists a resolution deduction of ?Q from ~?P
	i.e. there exists ?P1,...,?Pn=?Q such that ∀i,1≤i≤n, ?Pi is either
		a) a clause of ~?P, or
		b) a ground resolvent of two previous ?Pi's in the sequence
	We show, by induction on i, that ∀i, %5ε%1 ~?P⊃?Pi
	i=1:
	     ?P1 is a clause of ~?P  i.e. ~?P=?P1∧?Q1
	     ?P1 %5ε ?P1     Lemma 2
	     ?P1∧?Q1 %5ε ?P1     property 1 of definition of consequence ({yon(p2)}).
	     %5ε%1 (?P1∧?Q1)⊃?P1  Deduction theorem
	     %5.  ε%1 ~?P⊃?P1
.apart
.group;
	assume %5ε%1 ~?P⊃?Pi for i<k, then ?Pk is either: 
	  1) a clause of ~?P, or 
	  2) a ground resolvent of two previous ?Pi's
.end
.begin nofill;
             1) ~?P=?Pk∧?Qk, as above
		?Pk %5ε ?Pk          Lemma 2
		?Pk∧?Qk %5ε ?Pk
		%5ε%1 (?Pk∧?Qk)⊃?Pk   Deduction theorem
		i.e. %5ε%1 ~?P⊃?Pk
.apart
.group
	     2) ?Pk is a ground resolvent of ?Pi and ?Pj, i,j<k
		by the induction hypothesis, %5ε%1~?P⊃?Pi and %5ε%1~?P⊃?Pj
		thus, %5ε%1~?P⊃(?Pi∧?Pj)
		%5ε%1 (?Pi∧?Pj)⊃?Pk	Lemma 12
		%5ε %1~?P⊃?Pk		Lemma 4
	for i=n, we have %5ε%1 ~?P⊃?Pn but ?Pn=?Q
	%5.%1 ~?P%5*b%1 => %5ε%1~?P⊃?Q
.end


.group;
%7THEOREM 14%1  ~?P%5*b%1 => %5ε?P   

.BEGIN tabit1(15);
Proof:
	~?P%5*b%1 => there exists a resolution deduction ?P1,...,?Pn=%5b%1 of %5b%1 from ~?P  
.BEGIN FILL;INDENT 15,15;
	     1) %5b%1ε~?P => %5b%1=~?P   since ~?P is in reduced conjunctive
		form, then ?P=~(~?P)=~%5b%1=%5t%1.  Recall that %5t%1 is 
		an abbreviation for ~%dP%1∨%dP%1, which may also be written
       		%dP%1⊃%dP%1, thus ?P is simply %dP%1⊃%dP%1 which is
		provable by Lemma 2.

	     2) %5b%1 is ground resolvent of ?Pi and ?Pj, i,j<n; recall that
                %5b%* is an abbreviation for ~%dP%1∧%dP%1, thus
		by the proof of Lemma 13, we have
.END
\%5ε~?P⊃(%dP%1∧~%dP%1),   
\i.e. %5ε%1 ~?P⊃~(%dP%1⊃%dP%1)
\%5ε%dP%1⊃%dP%1		Lemma 2
\%5ε%1(%dP%1⊃%dP%1)⊃?P	Lemma 5
\%5. ε%1?P
.end

.apart
Thus for Propositional Logic, a statement is provable, iff it is true in
all models, iff its negation reduces to the empty clause by ground resolution.